Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		active(zeros)	→ mark(cons(0,zeros))
2:		active(tail(cons(X,XS)))	→ mark(XS)
3:		active(cons(X1,X2))	→ cons(active(X1),X2)
4:		active(tail(X))	→ tail(active(X))
5:		cons(mark(X1),X2)	→ mark(cons(X1,X2))
6:		tail(mark(X))	→ mark(tail(X))
7:		proper(zeros)	→ ok(zeros)
8:		proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
9:		proper(0)	→ ok(0)
10:		proper(tail(X))	→ tail(proper(X))
11:		cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
12:		tail(ok(X))	→ ok(tail(X))
13:		top(mark(X))	→ top(proper(X))
14:		top(ok(X))	→ top(active(X))

There are 18 dependency pairs:


15:		ACTIVE(zeros)	→ CONS(0,zeros)
16:		ACTIVE(cons(X1,X2))	→ CONS(active(X1),X2)
17:		ACTIVE(cons(X1,X2))	→ ACTIVE(X1)
18:		ACTIVE(tail(X))	→ TAIL(active(X))
19:		ACTIVE(tail(X))	→ ACTIVE(X)
20:		CONS(mark(X1),X2)	→ CONS(X1,X2)
21:		TAIL(mark(X))	→ TAIL(X)
22:		PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
23:		PROPER(cons(X1,X2))	→ PROPER(X1)
24:		PROPER(cons(X1,X2))	→ PROPER(X2)
25:		PROPER(tail(X))	→ TAIL(proper(X))
26:		PROPER(tail(X))	→ PROPER(X)
27:		CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
28:		TAIL(ok(X))	→ TAIL(X)
29:		TOP(mark(X))	→ TOP(proper(X))
30:		TOP(mark(X))	→ PROPER(X)
31:		TOP(ok(X))	→ TOP(active(X))
32:		TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 5 SCCs: {20,27}, {21,28}, {23,24,26}, {17,19} and {29,31}.

Consider the SCC {20,27}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 20 is weakly decreasing and rule 27 is strictly decreasing. There is one new SCC.
- Consider the SCC {20}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {21,28}. There are no usable rules. By taking the AF π with π(mark) = π(TAIL) = 1 together with the lexicographic path order with empty precedence, rule 21 is weakly decreasing and rule 28 is strictly decreasing. There is one new SCC.
- Consider the SCC {21}. By taking the AF π with π(TAIL) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.

Consider the SCC {23,24,26}. There are no usable rules. By taking the AF π with π(PROPER) = π(tail) = 1 together with the lexicographic path order with empty precedence, rule 26 is weakly decreasing and the rules in {23,24} are strictly decreasing. There is one new SCC.
- Consider the SCC {26}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 26 is strictly decreasing.

Consider the SCC {17,19}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 17 is weakly decreasing and rule 19 is strictly decreasing. There is one new SCC.
- Consider the SCC {17}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {29,31}. The usable rules are {1-12}. The constraints could not be solved.

Tyrolean Termination Tool (0.29 seconds) --- May 3, 2006